Problem:
 0(x1) -> 1(x1)
 4(5(4(5(x1)))) -> 4(4(5(5(x1))))
 5(5(5(5(5(5(4(4(4(4(4(4(x1)))))))))))) -> 2(x1)

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {5,4,3}
   transitions:
    11(10) -> 11*
    11(8) -> 9*
    00(2) -> 3*
    00(1) -> 3*
    10(2) -> 1*
    10(1) -> 1*
    40(2) -> 4*
    40(1) -> 4*
    50(2) -> 5*
    50(1) -> 5*
    20(2) -> 2*
    20(1) -> 2*
    1 -> 8*
    2 -> 10*
    9 -> 3*
    11 -> 3*
  problem:
   
  Qed